New file `Mathlib/Analysis/Calculus/LipschitzSmooth/Continuity.lean`. In a
finite-dimensional real inner-product space, a `K`-smooth function is locally
Lipschitz, hence continuous — without any convexity hypothesis on `f` and
without presupposing differentiability.

The proof routes through the **K-semiconcavity decomposition**: the upper-bound
side of the two-sided abs predicate implies `g(x) := f x - K/2 ‖x‖²` is
concave on the whole space (Cannarsa-Sinestrari, *Semiconcave Functions,
Hamilton-Jacobi Equations, and Optimal Control* (2004), Prop. 1.1.3(a)⇔(c)
p.2). Mathlib's `ConcaveOn.locallyLipschitz` (which requires
`[FiniteDimensional ℝ F]`) then gives local Lipschitz of `g`, and adding back
the locally Lipschitz `K/2 ‖x‖²` (via `ContDiff.locallyLipschitz` applied to
`contDiff_norm_sq`) recovers `f`.

The `[FiniteDimensional]` hypothesis is necessary: in infinite-dim, a
discontinuous linear functional `ℓ : F → ℝ` satisfies `LipschitzSmoothWith 0 ℓ`
but fails continuity (Bauschke-Combettes, *Convex Analysis and Monotone
Operator Theory in Hilbert Spaces* (2017), Example 8.42 p.151). The
`[InnerProductSpace]` restriction is for the parallelogram identity used in
the K-semiconcavity decomposition; a general-finite-dim-normed-space refinement
via norm-equivalence transfer is left as a follow-up.

Three theorems:
- `LipschitzSmoothWith.concaveOn_sub_half_sq_norm` — the semiconcavity
  decomposition (any dim, Hilbert).
- `LipschitzSmoothWith.locallyLipschitz` — corollary (finite-dim Hilbert).
- `LipschitzSmoothWith.continuous` — corollary (finite-dim Hilbert).

The full `C^{1,1}` characterisation (`Differentiable`, `LipschitzWith
(fderiv ℝ f)`) is deferred to a follow-up; it requires super-gradient
infrastructure not currently in mathlib.